%comment
\newcommand{\ignore}[1]{}
\newcommand{\etc}{etc.\ }

%formalism

%usefull
\newcommand{\set}[1]{\left\{#1\right\}}
\newcommand{\mset}[1]{\left[{#1}\right]}
\newcommand{\setcomp}[2]{\set{#1|\;#2}}
\newcommand{\tuple}[1]{\left(#1\right)}
\newcommand{\boolform}{{\mathbb B}}
\newcommand{\boolset}{{\cal B}}
\newcommand{\formula}{\theta}
\newcommand{\true}{{\it true}}
\newcommand{\false}{{\it false}}
\newcommand{\sfalse}{{\bf ff}}
\newcommand{\strue}{{\bf tt}}
\newcommand{\substitut}[1]{[{#1}]}
\newcommand{\imply}{\Rightarrow}
\newcommand{\undef}{\bot}
\newcommand{\nat}{{\cal N}}
\newcommand{\knat}{\set{0, 1, \ldots, k}}%{\nat^k}
\newcommand{\natform}{{\mathbb N}}
%\newcommand{\prefset}[1]{\overline{#1}}
\newcommand{\upto}[1]{\overline{#1}}
\newcommand{\injection}[3]{#1:\prefset{#2} \rightarrow \prefset{#3}}
\newcommand{\bin}[1]{\widetilde{#1}}
\newcommand{\instruction}{{\it instr}}
\newcommand{\condition}{{\it cond}}

%systems
\newcommand{\states}{Q}
\newcommand{\pstates}{P}
\newcommand{\var}{x}
\newcommand{\expr}{e}
\newcommand{\vars}{X}
\newcommand{\nvars}{Y}
\newcommand{\lvars}{\vars}
\newcommand{\transitions}{T}
\newcommand{\transition}{tr}
\newcommand{\btransition}{b}
\newcommand{\dtransition}{d}
\newcommand{\rtrpansition}{r}
\newcommand{\proc}{pr}
\newcommand{\state}{q}
\newcommand{\pstate}{p}
\newcommand{\lleft}{{\!L}}
\newcommand{\rright}{{\!R}}
\newcommand{\llrr}{{\!L\!R}}
\newcommand{\lforall}{\forall_\lleft}
\newcommand{\rforall}{\forall_\rright}
\newcommand{\lrforall}{\forall_\llrr}
\newcommand{\lexists}{\exists_\lleft}
\newcommand{\rexists}{\exists_\rright}
\newcommand{\lrexists}{\exists_\llrr}
\newcommand{\quant}{\Box}
\newcommand{\gcnds}{{\mathbb G}}
\newcommand{\guard}{{grd}}
\newcommand{\stmt}{{ stmt}}
\newcommand{\gcmd}{{\it cmd}}
\newcommand{\varstate}{v}
\newcommand{\lvarstate}{\varstate}
%\newcommand{\pstate}{u}
\newcommand{\svarstate}{\varstate}
\newcommand{\transrel}[1]{\stackrel{\raisebox{-2pt}{\scriptsize$#1$}}{\longrightarrow}}
\newcommand{\movesto}[1]{\stackrel{\raisebox{-2pt}{\scriptsize$#1$}}{\longrightarrow}}
\newcommand{\amovesto}[1]{\stackrel{\raisebox{-2pt}{\scriptsize$#1$}}{\longrightarrow_A}}
\newcommand{\kmovesto}[2]{\stackrel{\raisebox{-2pt}{\scriptsize$#2$}}{\longrightarrow_{#1}}}
\newcommand{\bmovesto}[1]{\stackrel{\raisebox{-2pt}{\scriptsize$#1$}}{\leadsto}}
\newcommand{\parsys}{{\cal P}}
\newcommand{\parsystuple}{\tuple{\states,\transitions}}
%\newcommand{\conf}{c}
\newcommand{\confs}{C}
\newcommand{\gconfs}{D}
\newcommand{\sconfs}{S}
\newcommand{\constrain}[2]{#1_{#2}}
\newcommand{\initlvarstate}{\varstate_{{\it init}}}
\newcommand{\initstate}{\state_{{\it init}}}
%\newcommand{\initprocstate}{\pstate_{{\it init}}}
\newcommand{\initprocstate}{\state_{{\it init}}}
\newcommand{\init}{{\it Init}}
\newcommand{\final}{\confs_F}
%\newcommand{\ts}{{\cal T}}
\newcommand{\gts}{{\cal T}}
\newcommand{\tstuple}{\tuple{\confs,\transrel{}}}
\newcommand{\gtstuple}{\tuple{\gconftsts,\gtransrel{}}}
\newcommand{\tsof}{{\cal T}}
\newcommand{\atsof}{{\cal A}}
\newcommand{\remove}{\ominus}
\newcommand{\atransrel}[1]{\stackrel{\raisebox{-2pt}{\scriptsize$#1$}}{\leadsto}}
\newcommand{\aatransrel}[1]{\stackrel{\raisebox{-2pt}{\!\!\!\scriptsize$#1$}}{\leadsto_1}}
\newcommand{\notmodels}{\nvDash}
\newcommand{\gvar}{g}
\newcommand{\svars}{S}
\newcommand{\sstate}{s}

%transition rule
\newcommand{\tr}[4]{%
\left [ \begin{array}{c}
#1 \\
#2 \rightarrow #3 \\
#4
\end{array}
\right ]
}

%constraints
\newcommand{\constrset}{\Psi}
\newcommand{\denotationof}[1]{\left[\!\left[#1\right]\!\right]}
\newcommand{\constr}{\phi}
\newcommand{\emptyconstr}{\epsilon}
\newcommand{\constrpre}{\it pre}
\newcommand{\constrs}{\Phi}
\newcommand{\entailed}{\sqsubseteq}
\newcommand{\pre}{\it Pre}
\newcommand{\post}{\it Post}
\newcommand{\fconstr}{\constr_F}
\newcommand{\fconstrs}{\constrs_F}
\newcommand{\urefine}{\otimes}
\newcommand{\erefine}{\oplus}
\newcommand{\rul}{\transition}
%\newcommand{\uc}[2]{\left(#1\right)\!\!\uparrow^{#2}}
%\newcommand{\frontier}[1]{{\cal{F}}_{#1}}


%model definition
\newcounter{modelboxcounter}
\setcounter{modelboxcounter}{0}
\newcommand{\modelbox}[6]{%
  \vspace{3mm}
  \noindent
  \framebox{
    \begin{minipage}{0.95\hsize}
      \noindent\underline{#1}

      \noindent{\bf Instance}

      \noindent{$\states$:} #2\\
      \noindent{$\vars$:} #3\\
      \noindent{$\transitions$:}
      {
        \small
        \begin{align*}
          #4
        \end{align*}
      }
      
      \noindent{\bf Initial Process State}
      \noindent{$\initprocstate$:} #5
      
      {\bf Final Constraints}
      {$\fconstrs$:} #6
    \end{minipage}
  }
  \vspace{2mm}
}

\newcommand{\modelboxg}[8]{%
  \vspace{3mm}
  \noindent
  \framebox{
    \begin{minipage}{0.95\hsize}
      \noindent\underline{#1}

      \noindent{\bf Instance}

      \noindent{$\states$:} #3\\
      \noindent{$\vars$:} #4\\
      \noindent{$\svars$:} #2\\
      \noindent{$\transitions$:}
      {
        \small
        \begin{align*}
          #5
        \end{align*}
      }

      \noindent{\bf Initial State of Shared Vars}
      \noindent{} #6
      
      \noindent{\bf Initial Process State}
      \noindent{$\initprocstate$:} #7

      {\bf Final Constraints}
      {$\fconstrs$:} #8
    \end{minipage}
  }
  \vspace{2mm}
}


%problem definition
\newcounter{probboxcounter}
\setcounter{probboxcounter}{0}
\newcommand{\probbox}[3]{%
  \vspace{3mm}
  \noindent
  \framebox{
    \begin{minipage}{0.95\hsize}
      \noindent\underline{#1}

      \noindent{\bf Instance}
      \vspace{-2mm}
      \begin{itemize}
        #2
      \end{itemize}
      \vspace{-2mm}
      \noindent{\bf Question}
      #3
    \end{minipage}
  }
  \vspace{2mm}
}


\newcommand{\acovproblem}{{\sc APRX-PAR-REACH}}
\newcommand{\covproblem}{{\sc PAR-REACH}}

%algorithm
\newcounter{algboxcounter}
\setcounter{algboxcounter}{0}
\newcommand{\algbox}[2]{%
  \refstepcounter{algboxcounter}
  \vspace{1mm}
  \noindent\framebox
  {
    %\small
    \begin{minipage}{0.95\hsize}
      {\bf Algorithm \thealgboxcounter{} -- #1}\\
      #2
    \end{minipage}
  }
  \vspace{1mm}
}

% draws a centered line and returns to the left margin. useful when
% the last line of a proof should contain a centered formula and a
% right-justified \qed
\newlength{\thintextcenterspacing}
\newcommand{\thintextcenter}[1]{%
  \settowidth{\thintextwidth}{#1}%
  \setlength{\thintextcenterspacing}{(85mm-\thintextwidth)/2}%
  ${}$\hspace{\thintextcenterspacing}\thintext{#1}\hspace{-\thintextcenterspacing}%
}

\newlength{\thintextwidth}
\newcommand{\thintext}[1]{%
  \settowidth{\thintextwidth}{#1}%
  {#1}\hspace{-\thintextwidth}%
}
\newcommand{\ind}{${}$\hspace{0.5cm}}
\newcommand{\algline}[1]{\thintext{#1}\ind}

\newcommand{\footnoteremember}[2]{

  \footnote{#2}
  \newcounter{#1}
  \setcounter{#1}{\value{footnote}}

} \newcommand{\footnoterecall}[1]{

  \footnotemark[\value{#1}]

}



\newcommand{\quantify}{\mathbb{Q}}


\newcommand{\numberof}[2]{\#{#1}\left(#2\right)}
\newcommand{\wordering}{\preceq}
\newcommand{\cntordering}[1]{\wordering^{#1}}
\newcommand{\cordering}{\sqsubseteq}
\newcommand{\cntcordering}{\cordering^\bullet}
\newcommand{\addstate}{\oplus}
\newcommand{\insertstate}{\otimes}
\newcommand{\removestates}{\ominus}
\newcommand{\sizeof}[1]{|#1|}
\newcommand{\wordof}[1]{{\it word}\left(#1\right)}

\newcommand{\statesof}[1]{\states\left(#1\right)}
\newcommand{\rstates}{R}
\newcommand{\shuffle}{\otimes}
\newcommand{\word}{w}
\newcommand{\symbolsof}[1]{{#1}^\bullet}
\newcommand{\proved}{\begin{flushright} $\Box$\end{flushright}}

\newcommand{\uc}[1]{\widehat{#1}}
\newcommand{\cuc}[2]{\widehat{#1}^{#2}}
\newcommand{\paddingset}{R}
\newcommand{\frontier}{{\cal{F}}}
\newcommand{\afrontier}{{\cal{AF}}}
\newcommand{\pred}[2]{{\bf pred}\left(#1,#2\right)}
\newcommand{\ppost}[2]{post\left(#1,#2\right)}

\newcommand{\isempty}{\cdot\ is\_empty}

\newcommand{\counter}[1]{{\cal C}_{#1}}
\newcommand{\assign}{{:=}}


\definecolor{myBrown}{rgb}{0.8,0.52,0.25}
\definecolor{myGreen}{rgb}{0.4,0.8,0}
\definecolor{myRed}{rgb}{0.8,0.36,0.36}
\definecolor{myBlue}{rgb}{0,0,1}
\definecolor{myPurple}{rgb}{0.4,0.35,0.8}

\newcommand{\redish}[1]{\textcolor{myRed}{#1}}
\newcommand{\greenish}[1]{\textcolor{myGreen}{#1}}
\newcommand{\brownish}[1]{\textcolor{myBrown}{#1}}
\newcommand{\bluish}[1]{\textcolor{myBlue}{#1}}
\newcommand{\purplish}[1]{\textcolor{myPurple}{#1}}



